(declare-fun fpv2 () Float32)
(declare-fun fpv3 () Float32)
(declare-fun fpv4 () Float32)
(declare-fun fpv5 () Float32)
(declare-fun fpv20 () Float32)
(declare-fun fpv32 () Float32)
(declare-fun fpv67 () Float32)
(declare-fun fpv82 () Float32)
(assert (fp.leq ((_ to_fp 8 24) RTN 0.108942357) ((_ to_fp 8 24) RTN 4536.57) fpv2))
(assert (fp.leq (fp.neg ((_ to_fp 8 24) RTN 753335.7)) (fp.min fpv3 (fp.mul RTN fpv4 (fp.neg fpv5)))))
(assert (or (fp.geq fpv67 (fp.div RTN fpv32 fpv20) fpv82 ((_ to_fp 8 24) RTN 0.805958)) (or false (fp.geq fpv3 (fp.max ((_ to_fp 8 24) RTN 753335.7) fpv5))) (fp.lt (_ +zero 8 24) (fp.sqrt RTN fpv4))))
(check-sat)
